%% DEFINITION ET DOMAINE
Toxicology~\cite{Waters2004} studies the adverse effects of the exposures to chemicals at various levels of living entities: organism, tissue, cell and intracellular molecular systems. During the last decade, the accumulation of genomic and post-genomic data together with the introduction of new technologies for gene analysis has opened the way to  \emph{toxicogenomics}. Toxicogenomics combines toxicology with 
``Omics'' technologies\footnote{“Omics” technologies are methodologies such as genomics, transcriptomics, proteomics and metabolomics.} 
to study the \emph{mode-of-action} of toxicants or environmental stressors on biological systems.
The mode-of-action is understood as the sequence of events from the absorption of chemicals to a toxic outcome.
Toxicogenomics potentially improves clinical diagnosis capabilities and facilitates the identification of potential toxicity  in drug discovery~\cite{Foster2007} or in the design of bio-synthetic entities~\cite{synthetic}. \looseness=-1

%% OBJECTIFS
The main approach used in toxicogenomics employs empirical analysis like in   the identification of molecular biomarkers, \ie indicators of disease or toxicity in the form of specific gene expression patterns~\cite{DeCristofaro2008}.
Clearly, biomarkers remain observational indicators linking genes related measures to toxic states. In this proposal, we complement these empirical methods with a computational technique  that aims at discovering the molecular mechanisms of toxicity. 
This  way, instead of studying the  phenomenology of the toxic impacts, we focus on the processes triggering adverse effects on organisms. 
Usually, the toxicity process  is defined as a sequence of physiological events that causes the abnormal behavior of a living organism  with respect to its healthy state.
Healthy physiological states generally correspond to homeostasis, namely a process that maintains a dynamic stability of internal conditions against changes in the external environment. 
Hence, we will consider toxicity outcomes as deregulation of homeostasis processes, namely deviation of some intrinsic referential equilibrium  of the system. \looseness=-1

Biological processes are usually given in terms of pathways which are  causal chains of the responses to stimuli, this way the deregulation of homeostasis  appears as the  activation or inhibition of  unexpected but existing pathways. Moreover, 
in the context of toxicogenomics it is crucial to take into account at least two other parameters: the exposure time  and the thresholds dosage delimiting the ranges of safe and hazardous effects.  

In this paper, we define a modular modeling environment, 
called \rnd for Reaction Networks with Delays,  depicting  the mechanistic process of toxicology. 
This model is build out of  a series of behavioral reactions among involved agents or species.  
Our work is influenced  by the definition of  reaction systems as given  in \cite{DBLP:journals/ijfcs/BrijderEMR11}. 
A reaction system is a set of \emph{reactions}, each of them defined as a triple $(R, I, P)$ where $R$ is the set of reactants, $I$ the set of inhibitors and $P$ the set of products, and $R,I$ and $P$ are taken from a common set of species \res. Reaction systems are based on three foundational principles: 
\begin{enumerate}[1.]
 \item \label{item:react} a reaction can take place only if all the reactants involved are available but none of the inhibitors is; 
 \item \label{item:quantity} if a species is available then a sufficient amount of it is present to trigger a reaction; \looseness=-1
 \item species are not persistent: they become unavailable if they are not sustained by a reaction.
\end{enumerate}

From this model we retain the idea of reactions but we significantly change the semantics. 
The first change concerns principle \ref{item:quantity}: species are available at a given discrete abstract  level. This is mainly related to the need of expressing toxicants doses. The corresponding  discretization is built observing thresholds levels in dose-response curves. 
The second and more fundamental change regards the introduction of discrete time constraints. Time plays a role in the evolution of species themselves and in the duration of reactions. 
More precisely, species are associated to a decay time $\delta$, meaning that their  level diminishes with time.
This accounts for the presence of a non-specified environment that consumes and degrades species, thus allowing to abstract away from reactions that may be neglected in the specified context.
Similarly, each reaction $(R, I, P)$ is extended with a response time $\Delta$ and  levels for all its reactants and inhibitors. 
Thus, principle \ref{item:react} is modified as follows: a reaction of response time $\Delta$ can take place only if each reactant stays at least at a given level and each involved inhibitor is at most at a given level during the whole reaction time. 
As a result, the  level of products of the reaction can be increased or decreased.



We model such systems into  high-level Petri nets.
The obtained network is compact and provides an intelligible graphical model of the described reactions. Moreover, the network is easily scalable: the size of the network grows linearly with the number of added species and reactions. Finally, by using high-level Petri nets, the model is prone to numerous extensions that are discussed in Section  \ref{sec:concl}. 

The second part of the paper is devoted to the analysis of toxicology via \rnd networks. We show how to  model toxicogenomics problems, namely deregulation of homeostatic processes, into formulae of a suitable temporal logic like CTL \cite{emerson}. It is therefore natural to address the satisfiability of these formulae using classic verification techniques such as model checking. 
 However, the introduction of time immediately renders the state space of \rnd networks infinite and standard model checking techniques cannot be applied directly. Nonetheless, we show that the automatic verification of formulae is possible as we provide  a correct and complete abstraction of  \rnd networks into Kripke structures.
We present both  \rnd networks and their encoded Kripke structures. The reason is that  the first one is modular and easily readable while the second one is much more intricate, less readable, and above all not scalable and not easily extensible. Moreover, this abstraction can be automatically generated from the \rnd network. 


All stages described above, starting from the modeling till the verification of the maintaining of the homeostasis,  are illustrated on a running example depicting  blood glucose regulation in human body. In particular, we highlight how the interplay between the assimilation of aspartame and glucose regulation causes the appearance of unwanted behaviors.

{\bf Organization of the paper.} 
The paper is organized as follows:  Section \ref{sec:petri} recalls basic definitions and notations on high-level Petri nets. Next, Section \ref{sec:example} describes our running example of blood glucose regulation. Section \ref{sec:reaction} introduces the principles behind \rnd networks and  presents their high-level Petri net modeling. Then Section \ref{sec:toxic} shows how to check toxicology properties in \rnd and states a sound and complete abstraction into Kripke structures.
Finally, Section \ref{sec:concl} discusses related works and concludes with some considerations on future work. \looseness=-1



